Language/OS - Multiplatform Resource Library/LANGUAGE OS.iso/ast_comp/concurre.tar/concurrency/README

Text File | 1993-07-05 | 27KB | 600 lines

          Papers on Foundations of Concurrency
                       Available by Anonymous FTP
                         from Boole.Stanford.EDU


This file is ABSTRACTS in the /pub directory of Boole.Stanford.EDU,
36.8.0.65, accessible by anonymous ftp.

The /pub directory is for FTP distribution of prepublications in the
area of foundations of concurrency.  It is run by the Boole group, a
subgroup of the Mathematical Theory of Computation group, Computer
Science Department, Stanford University.  The group consists of the
following people.

    Gidi Avrahami                   [e-mail]    (SYS)
        Carolyn Brown                   [e-mail]
    Rob van Glabbeek        [e-mail]
    Jeremy Gunawardena        [e-mail]
    Vineet Gupta            [e-mail]
    David Magerman                  [e-mail]
    Vaughan Pratt (group leader)    [e-mail]    (SYS)
    Marianne Siroker (secretary)    [e-mail]

==========================Instructions=================================

FTP LOGIN.  Give the following commands.

    ftp boole.stanford.edu
Login:    anonymous            (if you don't have an account on boole)
Paswd:    user@host            (your usual email address)
    bin                (if you are retrieving a .dvi file)
    prompt off            (if you want no ? prompts from mget)
    ls -ltr                (see what's there, most recent last)
    mget filename-1 ... filename-n    (e.g.   mget cg.tex es.tex dti.tex)
    quit                (exit from FTP)

SOURCE.  To retrieve the source to paper foo, get foo.tex.  The source
should be compiled using latex foo twice, the second time being to
resolve cross-references (if this annoys you let [e-mail]
know).  A third time may be necessary with particularly complex
documents, e.g. theses.

DVI.  If you wish to print paper foo without having to compile with
latex, first "cd DVI" then retrieve foo.dvi.  You must previously have
given the "bin" command to ftp since .dvi files are not text files.
Print foo.dvi on your host using

    lpr -d foo.dvi

We are considering not storing .dvi files in future.  If this would
inconvenience you, please let us know to what extent.  We make every
effort to avoid nonstandard macros and fonts.

PROBLEMS.  If you have problems in either retrieving or compiling
papers, please contact a systems person (flagged SYS on the list
above).

===========================Available papers=================================

TITLES

scbr.tex    The Second Calculus of Binary Relations
spectrum.ps The linear time - branching time spectrum II
complete.tex A complete ax'n for branching bisim. cong. of fin.state behaviours.
ql.tex      Linear Logic for Generalized Quantum Mechanics
dti.tex     The Duality of Time and Information
ldomain.tex Disjunctive Systems and L-Domains
monoidal.tex Some Monoidal Closed Categories of Stable Domains & Event Struct's
2d.tex      A Roadmap of Some Two-Dimensional Logics
ocbr.tex    Origins of the Calculus of Binary Relations
dalg.tex    Dynamic Algebras: Examples, Constructions, Applications
algecon.tex Arithmetic + Logic + Geometry = Concurrency
esrs.tex    Event Spaces and Related Structures
crewthes.tex Metric Process Models
atch.tex    Interleaving Semantics and Action Refinement with Atomic Choice
casthes.tex On the Specification of Concurrent Systems
es.tex      Event Spaces and their Linear Logic
cg.tex        Modeling Concurrency with Geometry
jelia.tex   Action Logic and Pure Induction
man.tex        Temporal Structures
pp2.tex        Teams Can See Pomsets
am4.tex        Enriched Categories and the Floyd-Warshall Connection
iowatr.tex  Dynamic Algebras as a well-behaved fragment of Relation Algebras
ijpp.tex    Modelling Concurrency with Partial Orders

-----------------------------------------------------------------------

ABSTRACTS

scbr.tex

        @InProceedings(
Pr93b,  Author="Pratt, V.R.",
        Title="The Second Calculus of Binary Relations",
        Booktitle="MFCS'93, Gda{\'{n}}sk", Address="Poland", Year=1993)

We view the Chu space interpretation of linear logic as an alternative
interpretation of the language of the Peirce calculus of binary
relations.  Chu spaces amount to K-valued binary relations, which for
K=2^n we show generalize n-ary relational structures.  We also exhibit
a four-stage unique factorization system for Chu transforms that
illuminates their operation.


spectrum.ps.Z
spectrum.A4.ps.Z

        @techreport{
vG92,   author=         "R.J. van Glabbeek",
        title =         "The linear time -- branching time spectrum II;
                        the semantics of sequential systems with silent moves",
        address =       Stanford,       year =          1993,
        note =          "Available by anonymous ftp from Boole.stanford.edu"}

This paper studies semantic equivalences and preorders for sequential
systems with silent moves, restricting attention to the ones that
abstract from successful termination, stochastic and real-time aspects
of the investigated systems, and the structure of the visible actions
systems can perform.  It provides a parameterized definition of a such
a preorder, such that most such preorders and equivalences found in
the literature are obtained by a suitable instantiation of the
parameters. Other instantiations yield preorders that combine
properties from various semantics. Moreover, the approach shows
several ways in which preorders that were originally only considered
for systems without silent moves, most notably the ready simulation,
can be generalized to an abstract setting. All preorders come
with---or rather as---a modal characterization, and when possible also
a relational characterization. Moreover they are motivated by means of
an (also parameterized) testing scenario, phrased in terms of `button
pushing experiments' on generative and reactive machines. The testing
scenarios for branching bisimulation, eta-bisimulation and coupled
simulation and the corresponding modal characterizations are
especially new.


complete.tex

        @TechReport(
vG92,   Author="R.J. van Glabbeek",
        Title ="A complete axiomatization for branching
                  bisimulation congruence of finite-state behaviours",
        Address=Stanford,
        Note="Available by anonymous ftp from Boole.stanford.edu", Year=1992)

This paper offers a complete inference system for branching
bisimulation congruence on a basic sublanguage of CCS for representing
regular processes with silent moves. Moreover, complete axiomatizations
are provided for the guarded expressions in this language, representing
the divergence- free processes, and for the recursion-free expressions,
representing the finite processes. Furthermore it is argued that in
abstract interleaving semantics (at least for finite processes)
branching bisimulation congruence is the finest reasonable congruence
possible.


ql.tex

        @InProceedings(
Pr93a,  Author="Pratt, V.R.",
        Title="Linear Logic for Generalized Quantum Mechanics",
        Booktitle="Proc. Workshop on Physics and Computation
        (PhysComp'92)", Address="Dallas", Publisher="{IEEE}", Year=1993)

Quantum logic is static, describing automata having uncertain states
but no state transitions and no Heisenberg uncertainty tradeoff.  We
cast Girard's linear logic in the role of a dynamic quantum logic,
regarded as an extension of quantum logic with time nonstandardly
interpreted over a domain of linear automata and their dual linear
schedules.  In this extension the uncertainty tradeoff emerges via the
``structure veil.'' When VLSI shrinks to where quantum effects are
felt, their computer-aided design systems may benefit from such logics
of computational behavior having a strong connection to quantum
mechanics.


dti.tex

    @InProceedings(
Pr92e,    Author="Pratt, V.R.",
    Title="The Duality of Time and Information",
    Booktitle="Proc. of CONCUR'92",
        Pages="?-?+16", Publisher="Springer-Verlag",
        Address="Stonybrook, New York", Month=Aug, Year=1992)

The states of a computing system bear information and change time,
while its events bear time and change information.  We develop a
primitive algebraic model of this duality of time and information for
rigid local computation, or straightline code, in the absence of choice
and concurrency, where time and information are linearly ordered.  This
shows the duality of computation to be more fundamental than the logic
of computation for which choice is disjunction and concurrency
conjunction.

To accommodate flexible distributed computing systems we then bring in
choice and concurrency and pass to partially ordered time and
information, the formal basis for this extension being Birkhoff-Stone
dualtiy.  A degree of freedom in how this is done permits a perfectly
symmetric logic of computation amounting to Girard's full linear logic,
which we view as the natural logic of computation when equal importance
is attached to choice and concurrency.

We conclude with an assessment of the prospects for extending the
duality to other organizations of time and information besides partial
orders in order to accommodate real time, nonmonotonic logic, and
automata that can forget, and speculate on the philosophical
significance of the duality.


monoidal.tex

    @Article(
Zh92a,  Author="Zhang, Guo-Qiang",
    Title="Some Monoidal Closed Categories of Stable Domains and
    Event Structures",
    Journal="Mathematical Structures in Computer Science",
    Year=1992(to appear))

This paper introduces the following new constructions on stable domains
and event structures: the tensor product, the linear function space,
and the exponential.  It results in a monoidal closed category of
dI-domains as well as one of stable event structures which can be used
to interpret intuitionistic linear logic.  Finally, the usefulness of
the category of stable event structures for modeling concurrency and
its relation to other models is discussed.


ldomain.tex

    @InProceedings(
Zh92b,    Author="Zhang, Guo-Qiang",
    Title="Disjunctive Systems and L-Domains",
    Booktitle="International Colloquium on Automata, Languages,
    and Programming", Address="Wien, Austria", Year=1992)

Disjunctive systems are a representation of L-domains.  They use
sequents of the form X|-Y, with X finite and Y pairwise disjoint.  We
show that for any disjunctive system, its elements ordered by inclusion
form an L-domain.  On the other hand, via the notion of stable
neighborhoods, every L-domain can be represented as a disjunctive
system.  More generally, we have a categorical equivalence between the
category of disjunctive systems and the category of L-domains.  A
natural classification of domains is obtained in terms of the style of
the entailment: when |X| = 2 and |Y| = 0, disjunctive systems determine
coherent spaces; when |Y| <= 1 they represent Scott domains; when
either |X| = 1 or |Y| = 0 the associated cpos are distributive Scott
domains; and finally, without any restriction, disjunctive systems give
rise to L-domains.


2d.tex

        @InProceedings(
Pr92c,  Author="Pratt, V.R.",
        Title="A Roadmap of Some Two-Dimensional Logics",
        Booktitle="Proc. of Workshop on Logic and the Flow of Information",
        Address="Amsterdam", Year=1992)

We define the notion of two-dimensional logic and diagram the relative
locations of a number of such.


ocbr.tex

        @InProceedings(
Pr92b,  Author="Pratt, V.R.",
        Title="Origins of the Calculus of Binary Relations",
        Booktitle="Proc. 7th Annual IEEE Symp. on Logic in Computer Science",
        Address="Santa Cruz, CA", Month=Jun, Year=1992)

The calculus of binary relations was introduced by De Morgan in 1860,
and was subsequently greatly developed by Peirce and Schroeder.  Half a
century later Tarski, J'onsson, Lyndon, and Monk further developed the
calculus from the perspective of modern model theory.


dalg.tex

    @Article(
Pr92d,    Author="Pratt, V.R.",
    Title="Dynamic Algebras: Examples, Constructions, Applications",
    Journal="Studia Logica", Year=1992)

Dynamic algebras combine the classes of Boolean (B + ' 0) and regular
(R U ; *) algebras into a single finitely axiomatized variety (B R <>)
resembling an R-module with ``scalar'' multiplication <>.  The basic
result is that * is reflexive transitive closure, contrary to the
intuition that this concept should require quantifiers for its
definition.  Using this result we give several examples of dynamic
algebras arising naturally in connection with additive functions,
binary relations, state trajectories, languages, and flowcharts.  The
main result is that free dynamic algebras are residually finite (i.e.
factor as a subdirect product of finite dynamic algebras), important
because finite separable dynamic algebras are isomorphic to Kripke
structures.  Applications include a new completeness proof for the
Segerberg axiomatization of propositional dynamic logic, and yet
another notion of regular algebra.


algecon.tex

        @InProceedings(
Pr92a,  Author="Pratt, V.R.",
        Title="Arithmetic + Logic + Geometry = Concurrency",
        Booktitle="Proc. First Latin American Symposium on Theoretical
                Informatics, LNCS 583",
        Pages="430-447", Publisher="Springer-Verlag",
        Address="Sao Paulo, Brazil", Month=Apr, Year=1992)

We relate the arithmetic of concurrent schedules to the
higher-dimensional cellular geometry of concurrent automata using the
logic of their Birkhoff-Stone duality.  This collects and unifies ideas
from several of the author's previous papers.


esrs.tex

    Event Spaces and Related Structures
    V.R. Pratt
    Manuscript, Stanford, 1992

This paper compares event spaces and their dual state spaces to some
related structures.  We emphasize their closest relative, event
structures, but also briefly consider coherence spaces and CPO's.  The
most significant contribution is the application of partial partitions
to the elementary description of Winskel's synchronous composition, but
the remarks on the advantages of state spaces over CPO's, in particular
Scott domains, for modeling fairness may also prove of interest.


crewthes.tex

        @PhDThesis(
Cre91,  Author="Roger Crew", Title="Metric Process Models",
        School="Stanford University", Month=Dec, Year=1991)

Among the various formal models proposed to provide semantics for
concurrency constructs in programming languages, partial orders have
the advantages of conceptual simplicity, mathematical tractability, and
economy of expression.  We first observe that the theory of enriched
categories supplies a natural abstraction of the notion of partial
order, the D-schedule.  Varying the choice of temporal domain D allows
for other forms of temporal constraint beyond that available from
simple ordering.  For example, having the constraints on inter-event
delays be numeric bounds produces a generalized metric-space structure
suitable for the discussion of real-time computation.  We then
construct an algebra of processes parametrized by notion of time.  Here
a process is a structure based on schedules that also incorporates
nondeterminism.  Since the model is category-based, we can define
operations on D-schedules and processes via universal constructions
that depend little on the choice of D.  Also, given a suitable choice
of process structure and process morphism, the constructions used for
process operations and schedule operations are remarkably similar.


atch.tex

    Interleaving Semantics and Action Refinement with Atomic Choice
    Rob van Glabbeek and Ursula Goltz
    To appear as Arbeitspapiere der GMD 594, Sankt Augustin,
    November 1991.

We investigate how to restrict the concept of action refinement such
that established interleaving equivalences for concurrent systems are
preserved under these restricted refinements.  We show that
interleaving bisimulation is preserved under refinement if we do not
allow to refine action occurrences deciding choices and action
occurrences involved in autoconcurrency.  On the other hand,
interleaving trace equivalence is still not preserved under these
restricted refinements.


casthes.tex

        @PhDThesis(
Cas91,  Author="Ross Casley",
        Title="On the Specification of Concurrent Systems",
        School="Stanford University", Month=Jan, Year=1991)

In models of concurrent processes constraints on the order of events are
often represented by partial orders, and schedules of events are then
defined using an algebra of standard operations such as sequential and
parallel composition.

In this dissertation the notion of partial order is replaced by that of a
set with a metric which takes values in a given ordered monoid.  Partial
orders are the simple case of a monoid whose two elements represent the
presence or absence of a constraint.

An ordered monoid can be seen as a monoidal category, and schedules based
on it are categories enriched in the monoid.  Algebraic operations on
schedules can then be defined as constructions in the category of
schedules.

These definitions rely on certain properties of a category of schedules,
such as closure and completeness.  To simplify proofs of these properties,
two constructions are defined.  The first creates a category of unlabeled
schedules from a system of constraints.  The second adds labels to
unlabeled schedules.  Many categories of interest can be constructed from
simple categories using these two methods.  The main results of the
dissertation derive the required properties of categories so constructed
from similar, more easily verified properties of the base categories.

Several notions of timing constraint can be viewed in a uniform way in
this framework.  An example is the Gaifman-Pratt system, essentially the
partial order model with additional specification as to whether two events
may occur simultaneously.  It corresponds to a monoid whose three elements
represent strict precedence, lax precedence (simultaneity is permitted),
and absence of constraint.  Real-valued timing constraints correspond to
the additive monoid of the real numbers.


es.tex

    @InProceedings(
Pr91b,    Author="Pratt, V.R.",
    Title="Event Spaces and Their Linear Logic",
    Booktitle="Proc. Second International Conference on Algebraic
        Methodology and Software Technology",
    Address="Iowa City", Month=May, Year=1991)

Boolean logic treats disjunction and conjunction symmetrically and
algebraically.  The corresponding operations for computation are
respectively nondeterminism (choice) and concurrency.  Petri nets treat
these symmetrically but not algebraically, while event structures treat
them algebraically but not symmetrically.

Here we achieve both via the notion of an event space as a poset with
all nonempty joins representing concurrence and a top representing the
unreachable event.  The symmetry is with the dual notion of state
space, a poset with all nonempty meets representing choice and a
bottom representing the start state.  The algebra is that of a parallel
programming language expanded to the language of full linear logic,
Girard's axiomatization of which is satisfied by the event space
interpretation of this language.

Event spaces resemble finite-dimensional vector spaces in
distinguishing tensor product from direct product and in being
isomorphic to their double dual, but differ from them in distinguishing
direct product from direct sum and tensor product from tensor sum.


cg.tex

    @InProceedings(
Pr91a,    Author="Pratt, V.R.",
    Title="Modeling Concurrency with Geometry",
    Booktitle="Proc. 18th Ann. ACM Symposium on Principles of
    Programming Languages", Pages="311-322",
    Month=Jan, Year=1991)

Branching time and causality find their respective homes in the
Birkhoff-dual models of automata and schedules.  This creates a
puzzle:  if the duality is supposed to make the models completely
equivalent then why does each phenomenon have a preferred side?  We
identify dimension as the culprit:  1-dimensional automata are
skeletons permitting only interleaving concurrency, true n-fold
concurrency resides in transitions of dimension n.  The Birkhoff dual
of a poset then becomes a simply-connected space.  We distinguish
Birkhoff duality from Stone duality and treat the former in detail from
a concurrency perspective.  We introduce true nondeterminism and define
it as monoidal homotopy; from this perspective nondeterminism in
ordinary automata arises from forking and joining creating nontrivial
homotopy.  We propose a formal definition of higher dimensional
automaton as an n-complex or n-category, whose two essential axioms are
associativity of concatenation within dimension and an interchange
principle between dimensions.


jelia.tex

    @InProceedings(
Pr90b,    Author="Pratt, V.R.",
    Title="Action Logic and Pure Induction",
    Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478",
    Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120",
    Address="Amsterdam, NL", Month=Sep, Year=1990)

In Floyd-Hoare logic programs are dynamic while assertions are static
(hold at states).  In action logic the two notions become one, with
programs viewed as on-the-fly assertions whose truth is evaluated along
intervals instead of at states.  Action logic is an equational theory
ACT conservatively extending the equational theory REG of regular
expressions with operations preimplication a -> b (HAD a THEN b) and
postimplication b <- a (b IF-EVER a).  Unlike REG, ACT is finitely
based, makes a* reflexive transitive closure, and has an equivalent
Hilbert system.  The crucial axiom is that of pure induction,
(a -> a)* = a -> a.


man.tex        Temporal Structures
        R. Casley, R. Crew, J. Meseguer, V. Pratt
        To appear in Mathematical Structures in Computer
        Science, 1:2.  Proceedings version in Category Theory
        and Computer Science, LNCS 389, Manchester, 1989.
        Formerly called "Dynamic Types."

We combine the principles of the Floyd-Warshall-Kleene algorithm,
enriched categories, and Birkhoff arithmetic, to yield a useful class
of algebras of transitive vertex-labeled spaces.  The motivating
application is a uniform theory of abstract or parametrized time in
which to any given notion of time there corresponds an algebra of
concurrent behaviors and their operations, always the same operations
but interpreted automatically and appropriately for that notion of
time.  An interesting side application is a language for succinctly
naming a wide range of datatypes.


pp2.tex        Teams Can See Pomsets
        G. Plotkin and V. Pratt
        Draft in preparation

Strings may serve as both specifications and observations of behavior.
However partial strings or pomsets, superior to strings in certain
respects for the representation of concurrent behavior, are provably
unobservable and hence apparently suitable only for specifying
behavior.  The proof however tacitly assumes that observers are
isolated individuals.  We show that observations by a cooperating team
of sequential observers agreeing on *what* happened but not
*when* can distinguish all pomsets.  The resolving power of a finite
team increases strictly with its size k, permitting it to distinguish
all pomsets of dimension (not width) k but not all of k+1.  These
results extend to observation of augment closed processes.  As expected
we depend on the now standard technique of refinement of atomic events
to complex events; what is not expected is that their complexity need
be only that of nondeterminism, in that we refine one atomic event to a
set of alternative atomic events, not to a set of sequences.


am4.tex

    @InProceedings(
Pr89a,    Author="Pratt, V.R.",
    Title="Enriched Categories and the {Floyd-Warshall} Connection",
    Booktitle="Proc. First International Conference on Algebraic
        Methodology and Software Technology",
    Pages="177-180", Address="Iowa City", Month=May, Year=1989)

We give a correspondence between enriched categories and the
Gauss-Kleene-Floyd-Warshall connection familiar to computer
scientists.  This correspondence shows this generalization of
categories to be a close cousin to the generalization of transitive
closure algorithms.  Via this connection we may bring categorical and
2-categorical constructions into an active but algebraically
impoverished arena presently served only by semiring constructions.  We
illustrate these techniques by applying them to Birkoff's poset
arithmetic, interpretable as an algebra of ``true concurrency.''


iowatr.tex

    @InProceedings(
Pr90a,    Author="Pratt, V.R.",
    Title="Dynamic Algebras as a Well-behaved Fragment of Relation
    Algebras",
    Booktitle="Algebraic Logic and Universal Algebra in Computer Science,
        LNCS 425",
    Editors="C.H. Bergman, R.D. Maddux, D.L. Pigozzi",
    Address="Ames, Iowa, June 1988",
    Publisher="Springer-Verlag", Year=1990)

The varieties RA of relation algebras and DA of dynamic algebras are
similar with regard to definitional capacity, admitting essentially the
same equational definitions of converse and star.  They differ with
regard to completeness and decidability.  The RA definitions that are
incomplete with respect to representable relation algebras, when
expressed in their DA form are complete with respect to representable
dynamic algebras.  Moreover, whereas the theory of RA is undecidable,
that of DA is decidable in exponential time.  These results follow from
representability of the free intensional dynamic algebras.


ijpp.tex

    @Article(
Pr86,    Author="Pratt, V.R.",
    Title="Modeling Concurrency with Partial Orders",
    Journal="Int. J. of Parallel Programming",
    Volume=15, Number=1, Pages="33-71", Month=Feb, Year=1986)

Concurrency has been expressed variously in terms of formal languages
(typically via the shuffle operator), partial orders, and temporal
logic, inter alia.  In this paper we extract from these three
approaches a single hybrid approach having a rich language that mixes
algebra and logic and having a natural class of models of concurrent
processes.  The heart of the approach is a notion of partial string
derived from the view of a string as a linearly ordered multiset by
relaxing the linearity constraint, thereby permitting partially ordered
multisets or pomsets.  Just as sets of strings form languages, so
do sets of pomsets form processes.  We introduce a number of operations
useful for specifying concurrent processes and demonstrate their
utility on some basic examples.  Although none of the operations is
particularly oriented to nets it is nevertheless possible to use them
to express processes constructed as a net of subprocesses, and more
generally as a system consisting of components.  The general benefits
of the approach are that it is conceptually straightforward, involves
fewer artificial constructs than many competing models of concurrency,
yet is applicable to a considerably wider range of types of systems,
including systems with buses and ethernets, analog systems, and
real-time systems.